FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
FormalTCS：评估 LLM 端到端理论计算机科学研究能力的基准
🧭 LLM 端到端科研能力评估
Harbin Institute of Technology
构建专家验证的 FormalTCS 基准，评估 LLM 在 STOC/FOCS/SODA/COLT 前沿 TCS 研究上的端到端能力，揭示自动形式化与科研品味是主要瓶颈。
📌 工作参考价值（3 点）
- 自动形式化是瓶颈：将自然语言需求转化为精确形式规范（如 SQL、DSL、策略规则）的能力远弱于在给定规范下的执行/证明能力。搭建 Agent 系统时，不要假设 LLM 能直接从模糊需求生成可执行逻辑，应设计中间表示或人工辅助的形式化步骤。
- 生成-过滤-证明流水线：采用“生成候选 → 自动过滤（规则/模型）→ 外部验证器（编译器、单元测试、仿真器）”的架构，将 LLM 生成和严格验证解耦，能显著提升最终输出质量。在推荐系统中，可用于自动生成策略规则、特征工程代码或查询重写规则，并用离线评估/在线 A/B 过滤。
- 评估基准设计：区分“给定形式化陈述的证明能力”与“从自然语言到形式化的转换能力”，避免用端到端指标掩盖子任务瓶颈。在业务中评估 LLM 能力时，应拆解为意图理解、结构化生成、逻辑推理等子任务分别评测。